P, Q:. Dec(P)  Dec(Q)  Dec(P & Q) 

latex

ProofTree

Definitions	t  T, P  Q, Dec(P), P  Q, , x:A. B(x), P & Q, A, False
Lemmas	not wf